Nuprl Lemma : cmconfig_wf
11,40
postcript
pdf
list
:(Id List). cmconfig(
list
)
chain_master()
latex
Definitions
cmconfig(
list
)
,
chain_master()
,
t
T
,
x
:
A
.
B
(
x
)
Lemmas
nat
wf
,
Id
wf
origin
list:(Id List). cmconfig(list) 
chain_master() list:(Id List). cmconfig(list) chain_master() Tx:A. B(x)